(0) Obligation:

Clauses:

times(X, Y, Z) :- mult(X, Y, 0, Z).
mult(0, Y, 0, 0).
mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z).
mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z).

Query: times(g,g,a)

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

(2) Obligation:

Clauses:

multA(0, 0).
multA(s(T63), T65) :- multA(T63, T65).
multB(0, s(0)).
multB(s(T119), s(T121)) :- multB(T119, T121).
multC(0, s(s(0))).
multC(s(T183), s(s(T185))) :- multC(T183, T185).
multD(0, s(s(s(0)))).
multD(s(T255), s(s(s(T257)))) :- multD(T255, T257).
multE(0, s(s(s(s(0))))).
multE(s(T335), s(s(s(s(T337))))) :- multE(T335, T337).
multF(0, s(s(s(s(s(0)))))).
multF(s(T423), s(s(s(s(s(T425)))))) :- multF(T423, T425).
multG(0, s(s(s(s(s(s(0))))))).
multG(s(T519), s(s(s(s(s(s(T521))))))) :- multG(T519, T521).
multH(0, s(s(s(s(s(s(s(0)))))))).
multH(s(T623), s(s(s(s(s(s(s(T625)))))))) :- multH(T623, T625).
multI(0, 0, 0).
multI(s(T51), 0, T54) :- multA(T51, T54).
multI(0, s(0), s(0)).
multI(s(T99), s(0), s(T102)) :- multB(T99, T102).
multI(0, s(s(0)), s(s(0))).
multI(s(T155), s(s(0)), s(s(T158))) :- multC(T155, T158).
multI(0, s(s(s(0))), s(s(s(0)))).
multI(s(T219), s(s(s(0))), s(s(s(T222)))) :- multD(T219, T222).
multI(0, s(s(s(s(0)))), s(s(s(s(0))))).
multI(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) :- multE(T291, T294).
multI(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))).
multI(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) :- multF(T371, T374).
multI(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))).
multI(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) :- multG(T459, T462).
multI(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))).
multI(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) :- multH(T555, T558).
multI(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) :- multJ(T635, s(s(s(s(s(s(s(T637))))))), T637, T639).
multJ(0, T649, 0, 0).
multJ(s(T662), T663, 0, T665) :- multI(T662, s(T663), T665).
multJ(T676, T677, s(T678), s(T680)) :- multJ(T676, T677, T678, T680).
timesK(0, T15, 0).
timesK(s(T28), T29, T31) :- multI(T28, T29, T31).

Query: timesK(g,g,a)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
timesK_in: (b,b,f)
multI_in: (b,b,f)
multA_in: (b,f)
multB_in: (b,f)
multC_in: (b,f)
multD_in: (b,f)
multE_in: (b,f)
multF_in: (b,f)
multG_in: (b,f)
multH_in: (b,f)
multJ_in: (b,b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TIMESK_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, multI_in_gga(T28, T29, T31))
TIMESK_IN_GGA(s(T28), T29, T31) → MULTI_IN_GGA(T28, T29, T31)
MULTI_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, multA_in_ga(T51, T54))
MULTI_IN_GGA(s(T51), 0, T54) → MULTA_IN_GA(T51, T54)
MULTA_IN_GA(s(T63), T65) → U1_GA(T63, T65, multA_in_ga(T63, T65))
MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)
MULTI_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, multB_in_ga(T99, T102))
MULTI_IN_GGA(s(T99), s(0), s(T102)) → MULTB_IN_GA(T99, T102)
MULTB_IN_GA(s(T119), s(T121)) → U2_GA(T119, T121, multB_in_ga(T119, T121))
MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U11_GGA(T155, T158, multC_in_ga(T155, T158))
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTC_IN_GA(T155, T158)
MULTC_IN_GA(s(T183), s(s(T185))) → U3_GA(T183, T185, multC_in_ga(T183, T185))
MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_GGA(T219, T222, multD_in_ga(T219, T222))
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTD_IN_GA(T219, T222)
MULTD_IN_GA(s(T255), s(s(s(T257)))) → U4_GA(T255, T257, multD_in_ga(T255, T257))
MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_GGA(T291, T294, multE_in_ga(T291, T294))
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTE_IN_GA(T291, T294)
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → U5_GA(T335, T337, multE_in_ga(T335, T337))
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_GGA(T371, T374, multF_in_ga(T371, T374))
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTF_IN_GA(T371, T374)
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U6_GA(T423, T425, multF_in_ga(T423, T425))
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_GGA(T459, T462, multG_in_ga(T459, T462))
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTG_IN_GA(T459, T462)
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U7_GA(T519, T521, multG_in_ga(T519, T521))
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_GGA(T555, T558, multH_in_ga(T555, T558))
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTH_IN_GA(T555, T558)
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_GA(T623, T625, multH_in_ga(T623, T625))
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_GGA(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → U18_GGGA(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → U19_GGGA(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
MULTI_IN_GGA(x1, x2, x3)  =  MULTI_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
MULTA_IN_GA(x1, x2)  =  MULTA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
MULTB_IN_GA(x1, x2)  =  MULTB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x3)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
MULTJ_IN_GGGA(x1, x2, x3, x4)  =  MULTJ_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4)  =  U18_GGGA(x4)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x5)

We have to consider all (P,R,Pi)-chains

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESK_IN_GGA(s(T28), T29, T31) → U20_GGA(T28, T29, T31, multI_in_gga(T28, T29, T31))
TIMESK_IN_GGA(s(T28), T29, T31) → MULTI_IN_GGA(T28, T29, T31)
MULTI_IN_GGA(s(T51), 0, T54) → U9_GGA(T51, T54, multA_in_ga(T51, T54))
MULTI_IN_GGA(s(T51), 0, T54) → MULTA_IN_GA(T51, T54)
MULTA_IN_GA(s(T63), T65) → U1_GA(T63, T65, multA_in_ga(T63, T65))
MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)
MULTI_IN_GGA(s(T99), s(0), s(T102)) → U10_GGA(T99, T102, multB_in_ga(T99, T102))
MULTI_IN_GGA(s(T99), s(0), s(T102)) → MULTB_IN_GA(T99, T102)
MULTB_IN_GA(s(T119), s(T121)) → U2_GA(T119, T121, multB_in_ga(T119, T121))
MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → U11_GGA(T155, T158, multC_in_ga(T155, T158))
MULTI_IN_GGA(s(T155), s(s(0)), s(s(T158))) → MULTC_IN_GA(T155, T158)
MULTC_IN_GA(s(T183), s(s(T185))) → U3_GA(T183, T185, multC_in_ga(T183, T185))
MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_GGA(T219, T222, multD_in_ga(T219, T222))
MULTI_IN_GGA(s(T219), s(s(s(0))), s(s(s(T222)))) → MULTD_IN_GA(T219, T222)
MULTD_IN_GA(s(T255), s(s(s(T257)))) → U4_GA(T255, T257, multD_in_ga(T255, T257))
MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_GGA(T291, T294, multE_in_ga(T291, T294))
MULTI_IN_GGA(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → MULTE_IN_GA(T291, T294)
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → U5_GA(T335, T337, multE_in_ga(T335, T337))
MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_GGA(T371, T374, multF_in_ga(T371, T374))
MULTI_IN_GGA(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → MULTF_IN_GA(T371, T374)
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → U6_GA(T423, T425, multF_in_ga(T423, T425))
MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_GGA(T459, T462, multG_in_ga(T459, T462))
MULTI_IN_GGA(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → MULTG_IN_GA(T459, T462)
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → U7_GA(T519, T521, multG_in_ga(T519, T521))
MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_GGA(T555, T558, multH_in_ga(T555, T558))
MULTI_IN_GGA(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → MULTH_IN_GA(T555, T558)
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_GA(T623, T625, multH_in_ga(T623, T625))
MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_GGA(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → U18_GGGA(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → U19_GGGA(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
MULTI_IN_GGA(x1, x2, x3)  =  MULTI_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
MULTA_IN_GA(x1, x2)  =  MULTA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
MULTB_IN_GA(x1, x2)  =  MULTB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x3)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x3)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x3)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x4)
MULTJ_IN_GGGA(x1, x2, x3, x4)  =  MULTJ_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4)  =  U18_GGGA(x4)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x5)

We have to consider all (P,R,Pi)-chains

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 9 SCCs with 29 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(T623), s(s(s(s(s(s(s(T625)))))))) → MULTH_IN_GA(T623, T625)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(12) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(T623)) → MULTH_IN_GA(T623)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTH_IN_GA(s(T623)) → MULTH_IN_GA(T623)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(T519), s(s(s(s(s(s(T521))))))) → MULTG_IN_GA(T519, T521)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(T519)) → MULTG_IN_GA(T519)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTG_IN_GA(s(T519)) → MULTG_IN_GA(T519)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(T423), s(s(s(s(s(T425)))))) → MULTF_IN_GA(T423, T425)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(T423)) → MULTF_IN_GA(T423)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTF_IN_GA(s(T423)) → MULTF_IN_GA(T423)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(31) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(T335), s(s(s(s(T337))))) → MULTE_IN_GA(T335, T337)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(T335)) → MULTE_IN_GA(T335)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTE_IN_GA(s(T335)) → MULTE_IN_GA(T335)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(39) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(T255), s(s(s(T257)))) → MULTD_IN_GA(T255, T257)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(40) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(T255)) → MULTD_IN_GA(T255)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(42) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTD_IN_GA(s(T255)) → MULTD_IN_GA(T255)
    The graph contains the following edges 1 > 1

(43) YES

(44) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(45) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(46) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(T183), s(s(T185))) → MULTC_IN_GA(T183, T185)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(47) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(48) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(T183)) → MULTC_IN_GA(T183)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(49) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTC_IN_GA(s(T183)) → MULTC_IN_GA(T183)
    The graph contains the following edges 1 > 1

(50) YES

(51) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTB_IN_GA(x1, x2)  =  MULTB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(52) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(53) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GA(s(T119), s(T121)) → MULTB_IN_GA(T119, T121)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTB_IN_GA(x1, x2)  =  MULTB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(54) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTB_IN_GA(s(T119)) → MULTB_IN_GA(T119)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(56) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTB_IN_GA(s(T119)) → MULTB_IN_GA(T119)
    The graph contains the following edges 1 > 1

(57) YES

(58) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTI_IN_GGA(x1, x2, x3)  =  MULTI_IN_GGA(x1, x2)
MULTJ_IN_GGGA(x1, x2, x3, x4)  =  MULTJ_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(59) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(60) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)
MULTJ_IN_GGGA(s(T662), T663, 0, T665) → MULTI_IN_GGA(T662, s(T663), T665)
MULTJ_IN_GGGA(T676, T677, s(T678), s(T680)) → MULTJ_IN_GGGA(T676, T677, T678, T680)

R is empty.
The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
MULTI_IN_GGA(x1, x2, x3)  =  MULTI_IN_GGA(x1, x2)
MULTJ_IN_GGGA(x1, x2, x3, x4)  =  MULTJ_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(61) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(62) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637)
MULTJ_IN_GGGA(s(T662), T663, 0) → MULTI_IN_GGA(T662, s(T663))
MULTJ_IN_GGGA(T676, T677, s(T678)) → MULTJ_IN_GGGA(T676, T677, T678)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(63) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTJ_IN_GGGA(s(T662), T663, 0) → MULTI_IN_GGA(T662, s(T663))
    The graph contains the following edges 1 > 1

  • MULTJ_IN_GGGA(T676, T677, s(T678)) → MULTJ_IN_GGGA(T676, T677, T678)
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

  • MULTI_IN_GGA(T635, s(s(s(s(s(s(s(s(T637))))))))) → MULTJ_IN_GGGA(T635, s(s(s(s(s(s(s(T637))))))), T637)
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(64) YES

(65) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)

The TRS R consists of the following rules:

timesK_in_gga(0, T15, 0) → timesK_out_gga(0, T15, 0)
timesK_in_gga(s(T28), T29, T31) → U20_gga(T28, T29, T31, multI_in_gga(T28, T29, T31))
multI_in_gga(0, 0, 0) → multI_out_gga(0, 0, 0)
multI_in_gga(s(T51), 0, T54) → U9_gga(T51, T54, multA_in_ga(T51, T54))
multA_in_ga(0, 0) → multA_out_ga(0, 0)
multA_in_ga(s(T63), T65) → U1_ga(T63, T65, multA_in_ga(T63, T65))
U1_ga(T63, T65, multA_out_ga(T63, T65)) → multA_out_ga(s(T63), T65)
U9_gga(T51, T54, multA_out_ga(T51, T54)) → multI_out_gga(s(T51), 0, T54)
multI_in_gga(0, s(0), s(0)) → multI_out_gga(0, s(0), s(0))
multI_in_gga(s(T99), s(0), s(T102)) → U10_gga(T99, T102, multB_in_ga(T99, T102))
multB_in_ga(0, s(0)) → multB_out_ga(0, s(0))
multB_in_ga(s(T119), s(T121)) → U2_ga(T119, T121, multB_in_ga(T119, T121))
U2_ga(T119, T121, multB_out_ga(T119, T121)) → multB_out_ga(s(T119), s(T121))
U10_gga(T99, T102, multB_out_ga(T99, T102)) → multI_out_gga(s(T99), s(0), s(T102))
multI_in_gga(0, s(s(0)), s(s(0))) → multI_out_gga(0, s(s(0)), s(s(0)))
multI_in_gga(s(T155), s(s(0)), s(s(T158))) → U11_gga(T155, T158, multC_in_ga(T155, T158))
multC_in_ga(0, s(s(0))) → multC_out_ga(0, s(s(0)))
multC_in_ga(s(T183), s(s(T185))) → U3_ga(T183, T185, multC_in_ga(T183, T185))
U3_ga(T183, T185, multC_out_ga(T183, T185)) → multC_out_ga(s(T183), s(s(T185)))
U11_gga(T155, T158, multC_out_ga(T155, T158)) → multI_out_gga(s(T155), s(s(0)), s(s(T158)))
multI_in_gga(0, s(s(s(0))), s(s(s(0)))) → multI_out_gga(0, s(s(s(0))), s(s(s(0))))
multI_in_gga(s(T219), s(s(s(0))), s(s(s(T222)))) → U12_gga(T219, T222, multD_in_ga(T219, T222))
multD_in_ga(0, s(s(s(0)))) → multD_out_ga(0, s(s(s(0))))
multD_in_ga(s(T255), s(s(s(T257)))) → U4_ga(T255, T257, multD_in_ga(T255, T257))
U4_ga(T255, T257, multD_out_ga(T255, T257)) → multD_out_ga(s(T255), s(s(s(T257))))
U12_gga(T219, T222, multD_out_ga(T219, T222)) → multI_out_gga(s(T219), s(s(s(0))), s(s(s(T222))))
multI_in_gga(0, s(s(s(s(0)))), s(s(s(s(0))))) → multI_out_gga(0, s(s(s(s(0)))), s(s(s(s(0)))))
multI_in_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294))))) → U13_gga(T291, T294, multE_in_ga(T291, T294))
multE_in_ga(0, s(s(s(s(0))))) → multE_out_ga(0, s(s(s(s(0)))))
multE_in_ga(s(T335), s(s(s(s(T337))))) → U5_ga(T335, T337, multE_in_ga(T335, T337))
U5_ga(T335, T337, multE_out_ga(T335, T337)) → multE_out_ga(s(T335), s(s(s(s(T337)))))
U13_gga(T291, T294, multE_out_ga(T291, T294)) → multI_out_gga(s(T291), s(s(s(s(0)))), s(s(s(s(T294)))))
multI_in_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))) → multI_out_gga(0, s(s(s(s(s(0))))), s(s(s(s(s(0))))))
multI_in_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374)))))) → U14_gga(T371, T374, multF_in_ga(T371, T374))
multF_in_ga(0, s(s(s(s(s(0)))))) → multF_out_ga(0, s(s(s(s(s(0))))))
multF_in_ga(s(T423), s(s(s(s(s(T425)))))) → U6_ga(T423, T425, multF_in_ga(T423, T425))
U6_ga(T423, T425, multF_out_ga(T423, T425)) → multF_out_ga(s(T423), s(s(s(s(s(T425))))))
U14_gga(T371, T374, multF_out_ga(T371, T374)) → multI_out_gga(s(T371), s(s(s(s(s(0))))), s(s(s(s(s(T374))))))
multI_in_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))) → multI_out_gga(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))))
multI_in_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462))))))) → U15_gga(T459, T462, multG_in_ga(T459, T462))
multG_in_ga(0, s(s(s(s(s(s(0))))))) → multG_out_ga(0, s(s(s(s(s(s(0)))))))
multG_in_ga(s(T519), s(s(s(s(s(s(T521))))))) → U7_ga(T519, T521, multG_in_ga(T519, T521))
U7_ga(T519, T521, multG_out_ga(T519, T521)) → multG_out_ga(s(T519), s(s(s(s(s(s(T521)))))))
U15_gga(T459, T462, multG_out_ga(T459, T462)) → multI_out_gga(s(T459), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(T462)))))))
multI_in_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))) → multI_out_gga(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))))
multI_in_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558)))))))) → U16_gga(T555, T558, multH_in_ga(T555, T558))
multH_in_ga(0, s(s(s(s(s(s(s(0)))))))) → multH_out_ga(0, s(s(s(s(s(s(s(0))))))))
multH_in_ga(s(T623), s(s(s(s(s(s(s(T625)))))))) → U8_ga(T623, T625, multH_in_ga(T623, T625))
U8_ga(T623, T625, multH_out_ga(T623, T625)) → multH_out_ga(s(T623), s(s(s(s(s(s(s(T625))))))))
U16_gga(T555, T558, multH_out_ga(T555, T558)) → multI_out_gga(s(T555), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(T558))))))))
multI_in_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639))))))))) → U17_gga(T635, T637, T639, multJ_in_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639))
multJ_in_ggga(0, T649, 0, 0) → multJ_out_ggga(0, T649, 0, 0)
multJ_in_ggga(s(T662), T663, 0, T665) → U18_ggga(T662, T663, T665, multI_in_gga(T662, s(T663), T665))
U18_ggga(T662, T663, T665, multI_out_gga(T662, s(T663), T665)) → multJ_out_ggga(s(T662), T663, 0, T665)
multJ_in_ggga(T676, T677, s(T678), s(T680)) → U19_ggga(T676, T677, T678, T680, multJ_in_ggga(T676, T677, T678, T680))
U19_ggga(T676, T677, T678, T680, multJ_out_ggga(T676, T677, T678, T680)) → multJ_out_ggga(T676, T677, s(T678), s(T680))
U17_gga(T635, T637, T639, multJ_out_ggga(T635, s(s(s(s(s(s(s(T637))))))), T637, T639)) → multI_out_gga(T635, s(s(s(s(s(s(s(s(T637)))))))), s(s(s(s(s(s(s(s(T639)))))))))
U20_gga(T28, T29, T31, multI_out_gga(T28, T29, T31)) → timesK_out_gga(s(T28), T29, T31)

The argument filtering Pi contains the following mapping:
timesK_in_gga(x1, x2, x3)  =  timesK_in_gga(x1, x2)
0  =  0
timesK_out_gga(x1, x2, x3)  =  timesK_out_gga(x3)
s(x1)  =  s(x1)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
multI_out_gga(x1, x2, x3)  =  multI_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multA_out_ga(x1, x2)  =  multA_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multB_out_ga(x1, x2)  =  multB_out_ga(x2)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U11_gga(x1, x2, x3)  =  U11_gga(x3)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multC_out_ga(x1, x2)  =  multC_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U12_gga(x1, x2, x3)  =  U12_gga(x3)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multD_out_ga(x1, x2)  =  multD_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multE_out_ga(x1, x2)  =  multE_out_ga(x2)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multF_out_ga(x1, x2)  =  multF_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multG_out_ga(x1, x2)  =  multG_out_ga(x2)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multH_out_ga(x1, x2)  =  multH_out_ga(x2)
U8_ga(x1, x2, x3)  =  U8_ga(x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x4)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
multJ_out_ggga(x1, x2, x3, x4)  =  multJ_out_ggga(x4)
U18_ggga(x1, x2, x3, x4)  =  U18_ggga(x4)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x5)
MULTA_IN_GA(x1, x2)  =  MULTA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(66) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(67) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTA_IN_GA(s(T63), T65) → MULTA_IN_GA(T63, T65)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTA_IN_GA(x1, x2)  =  MULTA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(68) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTA_IN_GA(s(T63)) → MULTA_IN_GA(T63)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(70) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • MULTA_IN_GA(s(T63)) → MULTA_IN_GA(T63)
    The graph contains the following edges 1 > 1

(71) YES